Termination w.r.t. Q of the following Term Rewriting System could be proven:

Q restricted rewrite system:
The TRS R consists of the following rules:

q0(0(x1)) → 0'(q1(x1))
q1(0(x1)) → 0(q1(x1))
q1(1'(x1)) → 1'(q1(x1))
0(q1(1(x1))) → q2(0(1'(x1)))
0'(q1(1(x1))) → q2(0'(1'(x1)))
1'(q1(1(x1))) → q2(1'(1'(x1)))
0(q2(0(x1))) → q2(0(0(x1)))
0'(q2(0(x1))) → q2(0'(0(x1)))
1'(q2(0(x1))) → q2(1'(0(x1)))
0(q2(1'(x1))) → q2(0(1'(x1)))
0'(q2(1'(x1))) → q2(0'(1'(x1)))
1'(q2(1'(x1))) → q2(1'(1'(x1)))
q2(0'(x1)) → 0'(q0(x1))
q0(1'(x1)) → 1'(q3(x1))
q3(1'(x1)) → 1'(q3(x1))
q3(b(x1)) → b(q4(x1))

Q is empty.


↳ QTRS
  ↳ DependencyPairsProof

Q restricted rewrite system:
The TRS R consists of the following rules:

q0(0(x1)) → 0'(q1(x1))
q1(0(x1)) → 0(q1(x1))
q1(1'(x1)) → 1'(q1(x1))
0(q1(1(x1))) → q2(0(1'(x1)))
0'(q1(1(x1))) → q2(0'(1'(x1)))
1'(q1(1(x1))) → q2(1'(1'(x1)))
0(q2(0(x1))) → q2(0(0(x1)))
0'(q2(0(x1))) → q2(0'(0(x1)))
1'(q2(0(x1))) → q2(1'(0(x1)))
0(q2(1'(x1))) → q2(0(1'(x1)))
0'(q2(1'(x1))) → q2(0'(1'(x1)))
1'(q2(1'(x1))) → q2(1'(1'(x1)))
q2(0'(x1)) → 0'(q0(x1))
q0(1'(x1)) → 1'(q3(x1))
q3(1'(x1)) → 1'(q3(x1))
q3(b(x1)) → b(q4(x1))

Q is empty.

Using Dependency Pairs [1,15] we result in the following initial DP problem:
Q DP problem:
The TRS P consists of the following rules:

1'1(q1(1(x1))) → 1'1(x1)
01(q2(0(x1))) → 01(0(x1))
Q3(1'(x1)) → Q3(x1)
1'1(q2(0(x1))) → 1'1(0(x1))
Q0(0(x1)) → Q1(x1)
Q2(0'(x1)) → Q0(x1)
Q1(0(x1)) → Q1(x1)
01(q2(1'(x1))) → Q2(0(1'(x1)))
0'1(q2(0(x1))) → Q2(0'(0(x1)))
1'1(q2(0(x1))) → Q2(1'(0(x1)))
Q1(1'(x1)) → 1'1(q1(x1))
Q1(1'(x1)) → Q1(x1)
01(q1(1(x1))) → Q2(0(1'(x1)))
0'1(q2(0(x1))) → 0'1(0(x1))
1'1(q2(1'(x1))) → Q2(1'(1'(x1)))
Q0(0(x1)) → 0'1(q1(x1))
1'1(q1(1(x1))) → Q2(1'(1'(x1)))
01(q1(1(x1))) → 1'1(x1)
0'1(q2(1'(x1))) → 0'1(1'(x1))
Q3(1'(x1)) → 1'1(q3(x1))
Q2(0'(x1)) → 0'1(q0(x1))
Q0(1'(x1)) → Q3(x1)
01(q1(1(x1))) → 01(1'(x1))
01(q2(1'(x1))) → 01(1'(x1))
0'1(q1(1(x1))) → Q2(0'(1'(x1)))
01(q2(0(x1))) → Q2(0(0(x1)))
Q0(1'(x1)) → 1'1(q3(x1))
1'1(q2(1'(x1))) → 1'1(1'(x1))
Q1(0(x1)) → 01(q1(x1))
1'1(q1(1(x1))) → 1'1(1'(x1))
0'1(q1(1(x1))) → 0'1(1'(x1))
0'1(q1(1(x1))) → 1'1(x1)
0'1(q2(1'(x1))) → Q2(0'(1'(x1)))

The TRS R consists of the following rules:

q0(0(x1)) → 0'(q1(x1))
q1(0(x1)) → 0(q1(x1))
q1(1'(x1)) → 1'(q1(x1))
0(q1(1(x1))) → q2(0(1'(x1)))
0'(q1(1(x1))) → q2(0'(1'(x1)))
1'(q1(1(x1))) → q2(1'(1'(x1)))
0(q2(0(x1))) → q2(0(0(x1)))
0'(q2(0(x1))) → q2(0'(0(x1)))
1'(q2(0(x1))) → q2(1'(0(x1)))
0(q2(1'(x1))) → q2(0(1'(x1)))
0'(q2(1'(x1))) → q2(0'(1'(x1)))
1'(q2(1'(x1))) → q2(1'(1'(x1)))
q2(0'(x1)) → 0'(q0(x1))
q0(1'(x1)) → 1'(q3(x1))
q3(1'(x1)) → 1'(q3(x1))
q3(b(x1)) → b(q4(x1))

Q is empty.
We have to consider all minimal (P,Q,R)-chains.

↳ QTRS
  ↳ DependencyPairsProof
    ↳ QDP
      ↳ QDPOrderProof

Q DP problem:
The TRS P consists of the following rules:

1'1(q1(1(x1))) → 1'1(x1)
01(q2(0(x1))) → 01(0(x1))
Q3(1'(x1)) → Q3(x1)
1'1(q2(0(x1))) → 1'1(0(x1))
Q0(0(x1)) → Q1(x1)
Q2(0'(x1)) → Q0(x1)
Q1(0(x1)) → Q1(x1)
01(q2(1'(x1))) → Q2(0(1'(x1)))
0'1(q2(0(x1))) → Q2(0'(0(x1)))
1'1(q2(0(x1))) → Q2(1'(0(x1)))
Q1(1'(x1)) → 1'1(q1(x1))
Q1(1'(x1)) → Q1(x1)
01(q1(1(x1))) → Q2(0(1'(x1)))
0'1(q2(0(x1))) → 0'1(0(x1))
1'1(q2(1'(x1))) → Q2(1'(1'(x1)))
Q0(0(x1)) → 0'1(q1(x1))
1'1(q1(1(x1))) → Q2(1'(1'(x1)))
01(q1(1(x1))) → 1'1(x1)
0'1(q2(1'(x1))) → 0'1(1'(x1))
Q3(1'(x1)) → 1'1(q3(x1))
Q2(0'(x1)) → 0'1(q0(x1))
Q0(1'(x1)) → Q3(x1)
01(q1(1(x1))) → 01(1'(x1))
01(q2(1'(x1))) → 01(1'(x1))
0'1(q1(1(x1))) → Q2(0'(1'(x1)))
01(q2(0(x1))) → Q2(0(0(x1)))
Q0(1'(x1)) → 1'1(q3(x1))
1'1(q2(1'(x1))) → 1'1(1'(x1))
Q1(0(x1)) → 01(q1(x1))
1'1(q1(1(x1))) → 1'1(1'(x1))
0'1(q1(1(x1))) → 0'1(1'(x1))
0'1(q1(1(x1))) → 1'1(x1)
0'1(q2(1'(x1))) → Q2(0'(1'(x1)))

The TRS R consists of the following rules:

q0(0(x1)) → 0'(q1(x1))
q1(0(x1)) → 0(q1(x1))
q1(1'(x1)) → 1'(q1(x1))
0(q1(1(x1))) → q2(0(1'(x1)))
0'(q1(1(x1))) → q2(0'(1'(x1)))
1'(q1(1(x1))) → q2(1'(1'(x1)))
0(q2(0(x1))) → q2(0(0(x1)))
0'(q2(0(x1))) → q2(0'(0(x1)))
1'(q2(0(x1))) → q2(1'(0(x1)))
0(q2(1'(x1))) → q2(0(1'(x1)))
0'(q2(1'(x1))) → q2(0'(1'(x1)))
1'(q2(1'(x1))) → q2(1'(1'(x1)))
q2(0'(x1)) → 0'(q0(x1))
q0(1'(x1)) → 1'(q3(x1))
q3(1'(x1)) → 1'(q3(x1))
q3(b(x1)) → b(q4(x1))

Q is empty.
We have to consider all minimal (P,Q,R)-chains.
We use the reduction pair processor [15].


The following pairs can be oriented strictly and are deleted.


1'1(q1(1(x1))) → 1'1(x1)
01(q2(0(x1))) → 01(0(x1))
1'1(q2(0(x1))) → 1'1(0(x1))
01(q2(1'(x1))) → Q2(0(1'(x1)))
0'1(q2(0(x1))) → Q2(0'(0(x1)))
1'1(q2(0(x1))) → Q2(1'(0(x1)))
01(q1(1(x1))) → Q2(0(1'(x1)))
0'1(q2(0(x1))) → 0'1(0(x1))
1'1(q2(1'(x1))) → Q2(1'(1'(x1)))
1'1(q1(1(x1))) → Q2(1'(1'(x1)))
01(q1(1(x1))) → 1'1(x1)
0'1(q2(1'(x1))) → 0'1(1'(x1))
01(q1(1(x1))) → 01(1'(x1))
01(q2(1'(x1))) → 01(1'(x1))
0'1(q1(1(x1))) → Q2(0'(1'(x1)))
01(q2(0(x1))) → Q2(0(0(x1)))
1'1(q2(1'(x1))) → 1'1(1'(x1))
1'1(q1(1(x1))) → 1'1(1'(x1))
0'1(q1(1(x1))) → 0'1(1'(x1))
0'1(q1(1(x1))) → 1'1(x1)
0'1(q2(1'(x1))) → Q2(0'(1'(x1)))
The remaining pairs can at least be oriented weakly.

Q3(1'(x1)) → Q3(x1)
Q0(0(x1)) → Q1(x1)
Q2(0'(x1)) → Q0(x1)
Q1(0(x1)) → Q1(x1)
Q1(1'(x1)) → 1'1(q1(x1))
Q1(1'(x1)) → Q1(x1)
Q0(0(x1)) → 0'1(q1(x1))
Q3(1'(x1)) → 1'1(q3(x1))
Q2(0'(x1)) → 0'1(q0(x1))
Q0(1'(x1)) → Q3(x1)
Q0(1'(x1)) → 1'1(q3(x1))
Q1(0(x1)) → 01(q1(x1))
Used ordering: Polynomial interpretation [25,35]:

POL(Q1(x1)) = (4)x_1   
POL(01(x1)) = (1/2)x_1   
POL(q0(x1)) = (4)x_1   
POL(1'1(x1)) = (1/2)x_1   
POL(0'(x1)) = (4)x_1   
POL(q2(x1)) = 1/4 + (4)x_1   
POL(b(x1)) = 0   
POL(Q0(x1)) = x_1   
POL(Q2(x1)) = (1/4)x_1   
POL(q3(x1)) = 0   
POL(q1(x1)) = (4)x_1   
POL(1(x1)) = 2 + (4)x_1   
POL(0'1(x1)) = (1/4)x_1   
POL(Q3(x1)) = 0   
POL(q4(x1)) = 0   
POL(1'(x1)) = (4)x_1   
POL(0(x1)) = (4)x_1   
The value of delta used in the strict ordering is 1/16.
The following usable rules [17] were oriented:

q0(0(x1)) → 0'(q1(x1))
q1(0(x1)) → 0(q1(x1))
1'(q1(1(x1))) → q2(1'(1'(x1)))
q1(1'(x1)) → 1'(q1(x1))
0(q1(1(x1))) → q2(0(1'(x1)))
1'(q2(0(x1))) → q2(1'(0(x1)))
0(q2(1'(x1))) → q2(0(1'(x1)))
0(q2(0(x1))) → q2(0(0(x1)))
0'(q1(1(x1))) → q2(0'(1'(x1)))
q2(0'(x1)) → 0'(q0(x1))
0'(q2(0(x1))) → q2(0'(0(x1)))
0'(q2(1'(x1))) → q2(0'(1'(x1)))
q0(1'(x1)) → 1'(q3(x1))
1'(q2(1'(x1))) → q2(1'(1'(x1)))
q3(b(x1)) → b(q4(x1))
q3(1'(x1)) → 1'(q3(x1))



↳ QTRS
  ↳ DependencyPairsProof
    ↳ QDP
      ↳ QDPOrderProof
        ↳ QDP
          ↳ DependencyGraphProof

Q DP problem:
The TRS P consists of the following rules:

Q1(0(x1)) → 01(q1(x1))
Q0(1'(x1)) → 1'1(q3(x1))
Q3(1'(x1)) → Q3(x1)
Q0(0(x1)) → Q1(x1)
Q1(0(x1)) → Q1(x1)
Q2(0'(x1)) → Q0(x1)
Q3(1'(x1)) → 1'1(q3(x1))
Q2(0'(x1)) → 0'1(q0(x1))
Q0(1'(x1)) → Q3(x1)
Q1(1'(x1)) → 1'1(q1(x1))
Q0(0(x1)) → 0'1(q1(x1))
Q1(1'(x1)) → Q1(x1)

The TRS R consists of the following rules:

q0(0(x1)) → 0'(q1(x1))
q1(0(x1)) → 0(q1(x1))
q1(1'(x1)) → 1'(q1(x1))
0(q1(1(x1))) → q2(0(1'(x1)))
0'(q1(1(x1))) → q2(0'(1'(x1)))
1'(q1(1(x1))) → q2(1'(1'(x1)))
0(q2(0(x1))) → q2(0(0(x1)))
0'(q2(0(x1))) → q2(0'(0(x1)))
1'(q2(0(x1))) → q2(1'(0(x1)))
0(q2(1'(x1))) → q2(0(1'(x1)))
0'(q2(1'(x1))) → q2(0'(1'(x1)))
1'(q2(1'(x1))) → q2(1'(1'(x1)))
q2(0'(x1)) → 0'(q0(x1))
q0(1'(x1)) → 1'(q3(x1))
q3(1'(x1)) → 1'(q3(x1))
q3(b(x1)) → b(q4(x1))

Q is empty.
We have to consider all minimal (P,Q,R)-chains.
The approximation of the Dependency Graph [15,17,22] contains 2 SCCs with 9 less nodes.

↳ QTRS
  ↳ DependencyPairsProof
    ↳ QDP
      ↳ QDPOrderProof
        ↳ QDP
          ↳ DependencyGraphProof
            ↳ AND
              ↳ QDP
                ↳ QDPOrderProof
              ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

Q1(0(x1)) → Q1(x1)
Q1(1'(x1)) → Q1(x1)

The TRS R consists of the following rules:

q0(0(x1)) → 0'(q1(x1))
q1(0(x1)) → 0(q1(x1))
q1(1'(x1)) → 1'(q1(x1))
0(q1(1(x1))) → q2(0(1'(x1)))
0'(q1(1(x1))) → q2(0'(1'(x1)))
1'(q1(1(x1))) → q2(1'(1'(x1)))
0(q2(0(x1))) → q2(0(0(x1)))
0'(q2(0(x1))) → q2(0'(0(x1)))
1'(q2(0(x1))) → q2(1'(0(x1)))
0(q2(1'(x1))) → q2(0(1'(x1)))
0'(q2(1'(x1))) → q2(0'(1'(x1)))
1'(q2(1'(x1))) → q2(1'(1'(x1)))
q2(0'(x1)) → 0'(q0(x1))
q0(1'(x1)) → 1'(q3(x1))
q3(1'(x1)) → 1'(q3(x1))
q3(b(x1)) → b(q4(x1))

Q is empty.
We have to consider all minimal (P,Q,R)-chains.
We use the reduction pair processor [15].


The following pairs can be oriented strictly and are deleted.


Q1(0(x1)) → Q1(x1)
Q1(1'(x1)) → Q1(x1)
The remaining pairs can at least be oriented weakly.
none
Used ordering: Polynomial interpretation [25,35]:

POL(Q1(x1)) = (4)x_1   
POL(1'(x1)) = 4 + (4)x_1   
POL(0(x1)) = 1 + x_1   
The value of delta used in the strict ordering is 4.
The following usable rules [17] were oriented: none



↳ QTRS
  ↳ DependencyPairsProof
    ↳ QDP
      ↳ QDPOrderProof
        ↳ QDP
          ↳ DependencyGraphProof
            ↳ AND
              ↳ QDP
                ↳ QDPOrderProof
                  ↳ QDP
                    ↳ PisEmptyProof
              ↳ QDP

Q DP problem:
P is empty.
The TRS R consists of the following rules:

q0(0(x1)) → 0'(q1(x1))
q1(0(x1)) → 0(q1(x1))
q1(1'(x1)) → 1'(q1(x1))
0(q1(1(x1))) → q2(0(1'(x1)))
0'(q1(1(x1))) → q2(0'(1'(x1)))
1'(q1(1(x1))) → q2(1'(1'(x1)))
0(q2(0(x1))) → q2(0(0(x1)))
0'(q2(0(x1))) → q2(0'(0(x1)))
1'(q2(0(x1))) → q2(1'(0(x1)))
0(q2(1'(x1))) → q2(0(1'(x1)))
0'(q2(1'(x1))) → q2(0'(1'(x1)))
1'(q2(1'(x1))) → q2(1'(1'(x1)))
q2(0'(x1)) → 0'(q0(x1))
q0(1'(x1)) → 1'(q3(x1))
q3(1'(x1)) → 1'(q3(x1))
q3(b(x1)) → b(q4(x1))

Q is empty.
We have to consider all minimal (P,Q,R)-chains.
The TRS P is empty. Hence, there is no (P,Q,R) chain.

↳ QTRS
  ↳ DependencyPairsProof
    ↳ QDP
      ↳ QDPOrderProof
        ↳ QDP
          ↳ DependencyGraphProof
            ↳ AND
              ↳ QDP
              ↳ QDP
                ↳ QDPOrderProof

Q DP problem:
The TRS P consists of the following rules:

Q3(1'(x1)) → Q3(x1)

The TRS R consists of the following rules:

q0(0(x1)) → 0'(q1(x1))
q1(0(x1)) → 0(q1(x1))
q1(1'(x1)) → 1'(q1(x1))
0(q1(1(x1))) → q2(0(1'(x1)))
0'(q1(1(x1))) → q2(0'(1'(x1)))
1'(q1(1(x1))) → q2(1'(1'(x1)))
0(q2(0(x1))) → q2(0(0(x1)))
0'(q2(0(x1))) → q2(0'(0(x1)))
1'(q2(0(x1))) → q2(1'(0(x1)))
0(q2(1'(x1))) → q2(0(1'(x1)))
0'(q2(1'(x1))) → q2(0'(1'(x1)))
1'(q2(1'(x1))) → q2(1'(1'(x1)))
q2(0'(x1)) → 0'(q0(x1))
q0(1'(x1)) → 1'(q3(x1))
q3(1'(x1)) → 1'(q3(x1))
q3(b(x1)) → b(q4(x1))

Q is empty.
We have to consider all minimal (P,Q,R)-chains.
We use the reduction pair processor [15].


The following pairs can be oriented strictly and are deleted.


Q3(1'(x1)) → Q3(x1)
The remaining pairs can at least be oriented weakly.
none
Used ordering: Polynomial interpretation [25,35]:

POL(Q3(x1)) = (1/4)x_1   
POL(1'(x1)) = 1/4 + (2)x_1   
The value of delta used in the strict ordering is 1/16.
The following usable rules [17] were oriented: none



↳ QTRS
  ↳ DependencyPairsProof
    ↳ QDP
      ↳ QDPOrderProof
        ↳ QDP
          ↳ DependencyGraphProof
            ↳ AND
              ↳ QDP
              ↳ QDP
                ↳ QDPOrderProof
                  ↳ QDP
                    ↳ PisEmptyProof

Q DP problem:
P is empty.
The TRS R consists of the following rules:

q0(0(x1)) → 0'(q1(x1))
q1(0(x1)) → 0(q1(x1))
q1(1'(x1)) → 1'(q1(x1))
0(q1(1(x1))) → q2(0(1'(x1)))
0'(q1(1(x1))) → q2(0'(1'(x1)))
1'(q1(1(x1))) → q2(1'(1'(x1)))
0(q2(0(x1))) → q2(0(0(x1)))
0'(q2(0(x1))) → q2(0'(0(x1)))
1'(q2(0(x1))) → q2(1'(0(x1)))
0(q2(1'(x1))) → q2(0(1'(x1)))
0'(q2(1'(x1))) → q2(0'(1'(x1)))
1'(q2(1'(x1))) → q2(1'(1'(x1)))
q2(0'(x1)) → 0'(q0(x1))
q0(1'(x1)) → 1'(q3(x1))
q3(1'(x1)) → 1'(q3(x1))
q3(b(x1)) → b(q4(x1))

Q is empty.
We have to consider all minimal (P,Q,R)-chains.
The TRS P is empty. Hence, there is no (P,Q,R) chain.